(set-option :produce-models true)
(set-logic QF_SLIA)
(set-info :status sat)
(declare-const x String)

(assert
 (str.in_re
  x
  (re.++
   (str.to_re "pref")
   (re.* re.allchar)
   (str.to_re "a")
   (re.* re.allchar)
   (str.to_re "b")
   (re.* re.allchar)
   (str.to_re "c")
   (re.* re.allchar)
   (str.to_re "d")
   (re.* re.allchar)
   (str.to_re "e")
   (re.* re.allchar)
   (str.to_re "f")
   (re.* re.allchar)
   (str.to_re "g")
   (re.* re.allchar)
   (str.to_re "h")
   (re.* re.allchar)
   (str.to_re "i")
   (re.* re.allchar)
   (str.to_re "j")
   (re.* re.allchar)
   (str.to_re "k")
   (re.* re.allchar)
   (str.to_re "l")
   (re.* re.allchar)
   (str.to_re "m")
   (re.* re.allchar)
   (str.to_re "n")
   (re.* re.allchar)
   (str.to_re "o")
   (re.* re.allchar)
   (str.to_re "p")
   (re.* re.allchar)
   (str.to_re "q")
   (re.* re.allchar)
   (str.to_re "r")
   (re.* re.allchar)
   (str.to_re "s")
   (re.* re.allchar)
   (str.to_re "t")
   (re.* re.allchar)
   (str.to_re "u")
   (re.* re.allchar)
   (str.to_re "v")
   (re.* re.allchar)
   (str.to_re "w")
   (re.* re.allchar)
   (str.to_re "x")
   (re.* re.allchar)
   (str.to_re "y")
   (re.* re.allchar)
   (str.to_re "z")
   (re.* re.allchar))))

(assert
 (or
  (= x "pref0a-b-c-de")
  (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar)))
  (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar)))))

(check-sat)


